COMMENT ⊗   VALID 00009 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.device XGP
C00004 00003	.onecol BEGIN "TITLE PAGE"
C00005 00004	.BEGIN "COVER PAGE"
C00008 00005	.EVERY HEADING(%3{SECNAME},{SSNAME},{PAGE!}) page←0 twocol cb Abstract
C00044 00006	.cb Personnel
C00051 00007	.onecol cb Budget
C00056 00008	.twocol bib
C00058 00009	.skip 200
C00060 ENDMK
C⊗;
.device XGP;
.require "bask.pub[sub,sys]" source_file;
.font 5 "gacs25";
.font 6 "clar30"
.font 9 "sail25"
.sides←1;
.require "twocol.pub[sub,sys]" source_file;

.MACRO YON(LBL)  ⊂ "Section "; SUB2! LBL ⊃;

.MACRO BC ⊂ BEGIN PREFACE 0; INDENT 1,4; CRBREAK nojust ⊃

.MACRO BS ⊂ BEGIN PREFACE 0; INDENT 1,4; nojust ⊃

.MACRO SUB(IND) ⊂ INDENT 0,IND; TABS IND+1;⊃

.MACRO IB ⊂ turn on "%";
.AT """" ⊂ (IF THISFONT=1 THEN "%3" ELSE "%1"); ⊃
.AT "<" ⊂ "%2" ⊃;  AT ">" ⊂ "%1" ⊃;
. ⊃

.MACRO BIB  ⊂  CB(References);
.	BEGIN INDENT 0,3; NOJUST; IB;
.	AT "AIM-" ⊂ "Stanford AI Memo AαIαMα-" ⊃;
.	COUNT exref TO 200
.	AT "⊗" ⊂ IF LINES<3 THEN NEXT COLUMN; NEXT EXREF; ("["&EXREF&"]  ") ⊃
.	⊃
.
.COUNT ITEM
.AT "#" ⊂NEXT ITEM;(ITEM!);⊃;

.SECNAME←"";
.portion some; place text;
.every heading();
.`∨]∃G←Xvαα
ε≡Lq↓
RM"2∃ααλ∀<*!Q"u≤9~α¬$βh⊂iyα*fgλ_]FE!bg*⊃i≥FE()"c⊂abP_∞FA↔)Qf"ajλ_YFE∀2yrp\αch Proposal Submitted to
.CKIP 2l~∀JgQ⊃∃αt
R&>t
1αN≤J⊗*∞*α~>Vt"εR→y`hRh∧ri~λ@≥CE∩Xs≠y
.SKIP 2;
%3Bas@%BA%KMKCeG AS\A¬aiSMαK∂'πbα';S,c3'∨.s∂∀∀RrN.&α↓Il4R)GdhQ:N.M↓↓IlhR+?#rα7∞∂∂∪S#dhRCK?6+OO?∩β?2λ9voπ↑LW∩¬<=⊗.v<QPUπ-≥f≡O≥B∧NnlW∨&≤|↔&␈!Q"u≤9~αβC1Q$W.O∀βKvqPRu99∃αβW1PT≡⎇↑π/&↑$¬≡≡≤]f≡
λLWε∂.MV.wAQ"u≤9~αβ1Q"+≥:H∀t4z(B¬,i~d-∃9~EHh%j4\M∧ε∪Xh$V∃∨&≥lf␈⊗ED∧≡∞M≤f␈⊗m≤⊂hRhYd"α*I∃$dT
∧<T'0hPbt(XtLr∧(4⎇4Z$¬∧xT hRj94Mα
Ir∧≤yJTlrε↔0hRiit4LIG0hRj
$,4_8Rββ1Q"tLhHTu"ε¬Cαcπ1PRu8YD,≥Dε∪Xh%jE-∀d	trα+@⊃B∪1Q"t
D∧!ab$
EE"∧#R∩↓∧∂`	BW~EE"U#∂Zα↔0hRa_$,<→dα∀≤zhU∩¬λ_t*¬I~Dd*!Q"pL8Ye$-'1PRp~8Td,:Dβ3XQ*&/≡\≡&≡B
∞&␈ε}<⊗b¬>\&nONLV"πMtπ&FT	f∂&≥⎇f∞b
<6N.l<R∧6}]f&∂M≥vph%a∀,tD∧$≤⎇hZ"¬∧_xR¬$~ID*∪1Q"u≤9~αβ+1Q"u≤YHT≥"ε↔0hU∞-wε␈<\B∧∞]}Vw"βCB'G¬OπGAT
π⊗␈
}6."λ\f6.>M↔6*λL↔&*βCC
∧,≥brβ↔⊗sAj
∞&␈ε}<V"∧N↑&∂&≥⎇b↓aF4πN.≡.1hh%j4\M∧ε3Xh*M↔&fTβAd⊗≡=⊗~¬,↑6.∂,=αεNdλ↔↔&≤m⊗≡N≥D∧NwL]FfN|]f≡)QQ"u$_*2β#π1PRu99∃αβ71PUπ-≥f≡O≥B∧NnlW∨&≤|↔&␈$βAdV⎇
b∧n8<↔↔&∂∪Ue∨\-VO'M≥f:∧≥n7&ON↑FN}dβAe∨L≥f6␈,D¬.v≡lW↔≡≡O⊃hh$∧¬≡}5d¬≡.5d∧vzdβAc+W¬S≠αV@
g⊗g7⊃↑_<]
\;]⊂π∞⊂!w[x:z2\⊂)qdYw1rPλ⊂⊂∞FB. r2≤2yyPπ∞)z0[37y2⊂!pv~s7y7~pP≤ZX~NFB↔)edT⊂→]FB&purH3y0w≥⊂:7Pπ∞!7p\2⊂7sλ*9:y]2ryP≠pε the Leland StanfOrd Junior UnivErsity≥
α.SKIP 3;
EndorsEments:
.TABS 10,35,59;
.SKIP 1;
\Principal Investigator\DepartmentHead\Institqtional Admin. Official
.TABS 10,35,60;
.PR@
β
@bv4∃≥C[∃88 2T{#)αn~∂πK&Ce↓↓α↓↓↓↓↓jppR.#←πK"α¬9α6+'∨↔v∪πW5↓jppQα↓↓↓↓α↓↓↓↓α↓↓↓↓α↓↓↓↓↓h4):≤Z&A↓	X4*ON;;πS,ε&-aCDααα∧∧ααα∧∧ααα∧∧ααα∧∧↓maCDααα∧∧ααα∧∧ααα∧∧ααα∧∧↓maCDααα∧∧ααα∧∧ααα∧∧ααα∧∧↓hh*M↔&f[CAeπ-|f/∨=}"αα∧∧ααα∧∧αα↓[CAeπ-|f/∨=}"α2λ=ε∞O-\⊗r↓[CAbα∧∧ααα∧∧ααα∧∧ααα∧∧αα↓QQ%&.L↑εF}l[AabεB∪*JεG∪:kFF3αα∧∧αααβ[AabεB∪*JεC∪:kFεsJα∧∧αααβ[Aab∧∧ααα∧∧ααα∧∧ααα∧∧αααβQPT&≡LUaaD∧ααα∧∧ααα∧∧ααα∧∧ααα∧βUaaD∧ααα∧∧ααα∧∧ααα∧∧ααα∧βUaaD∧ααα∧∧ααα∧∧ααα∧∧ααα∧βPhRhYd"α(9u4-$
∧<T'0hPbtZhU∃J	λT$α3Qe∧,}thXsP3(←K_
iTdεAME},{@AGE!}$p
βC∞;⊗⎇AX∧π'>|8mGh_xDλ8\p~≤αact
.fi@1XACI)kgh~(∪)QSLASfA∧AeKcUKghAα37Iβλ∧ε >X;U↓PZ;@⊂≤zx8 /ppλA←_AECgαK¬βK/≠↔πK≡Aβ'→∧∧↔.~9P∀Xtpv⊂~w:2`,ligenca~∃β;'S!∧∧VOε≡6O~
⎇bπ&Tπ∨'.XλnNαy2P≠pε f@=aSCX↓eKCgα{;'lpλ≥Yβ"L={<⊂~]2y⊂(≤αogf `πQKG-S]N\A)QJ↓G←[aUiKdAA`?∨2βπ#↔≡[';≥π≠WCC⎇∪SMβ&C∀4,,↔=8h→→yrpy_t⊂4wλ dV⊂_8¬t also has applicAtions to verifYing
compUter @AeP∨∨⊗7Mβ∞s⊃β'~β';∪/β↔;∪,sS3@∀
f∞g\≤&f*aQ hRl<"∧NnN&}π\8

≥{C"AP@∧`y≥4s4aZpp %]`∪↔`¬FNy;XlT~_<d∞≤[⎇L\λ≥≠dY(_$~9@3~qzv 4 branch
Od scIence.  So@5JAaKα{C &T


⎇9z∞D≥~_.D~≥0⊗Xw⊂6 %ve`_AαK;@&]@≠
≤βrw1YF@
c@=kYHAα∪∃βπ≡C'/l\BεNdλ
]H≠`9λ:;rg≥<P<`%ars, bphAβ##'M∧εv∂~,↔≡∞Dλma ¬:4→P24`&d¬SGkαcS'↔~βS#↔Jβ∂?Wd!βO↔*βW#↔p∧π&F←∀εn∞LTπ&FTλn∞~;:.>~8c!.≤Y9
≤⎇~0↔[9W⊂⊂∪zy⊂ /wn oPin`∪←8ASfAQQChA5CU←@∩βO∂',sS'≠N→β∪'≤∧6␈6↑-⊗/_Q*&.n≥≥bπ&t&*ε\≤F*pβ"S-}Y;⎇L↑Kλ≠,≥↑(≠ld≥~→.<αP24\qws2\4ryP≤2xz`)re theore@QSGCX↓CImC9G@↔Mε;⊂4Vs?Qβn+K↔3JβS#∃∧+cS↔w≠'?9ε{⊃β∂,ε'⊗.nDεN&\≡2ε6} λ∞∞[y≥,=;Yh∧,>≤⊃..λ≤⊂→≠sy0v\QαE*≠P72kH27vpZw9WεB*42P~w1y2Xytw3H2vx4_ytyP_<P i∀ P0w→⊂7z4→y⊂0sYw1tr\β sp@=]g←e%]NAβ$~∃eKMKCeG A←\A%[[KI%CiJA¬aaYSα≠πS'}sMβ#∂→βK↔≥+3S↔ β'9βλβO/-→w/_Q-⊗n⊗≥L⊗v≡Udα∧&\8
,M;Y`∞⎇_=∞M→(_L≡z8h
≡|⎇0∩\P0y2H4yP2~s34q]v:εE→w7zsZ⊂;tz~7zz~0{4w→P37y≠zv0z→P2{ %rything in termq of demonstration
programs to be available in two years.

	Our research is based on the idea that for many purposes,
the problems of artificial intelligence can be separated into two
parts - an epistemological part anda heuristic part.¬
The %2epistemoloeical%1 part concernq what facts and inference
αrules are availabstic part
concerns procedures for deciding what to do on the basis of the
necessary facts.  Most work in AI has concerned the %2heuristics%1,
and compu@QKdAe∃aeKgα+;@&≡M⊗}w4
v2ε≥lf␈⊗\≡FN}d
ε∂6T&..dλ6F␈<]bπ&≡@hV≡,Rε≡≡λ⊗⊗@→(≠lD≤Y<∞,<y;NM9Y`
⎇[≡(∀≤_<ND≠yH∞M→(∩-lY|[,≡~;{D∞~_=↓Q]{⎇-Lλ_Y$=X:-L8[⊂∩H:7P0H4:vp[↔⊂⊂*~2P6wY2yP7Y⊂92p\ww4w→β us@∃HAEr4∃aeKMK]hAAeP∨∨⊗7Mβ∂∪∃β?0εF.rZf.r∞|V∞↑↑ λ∞M_;@∞M→(⊂→→x92yYw:0z~ww9FB:42v\rv; %s*~∀4∀∪)Q∀AYS]∃bA←L↓eKgK¬`∂!∧εv*π
L⊗rπMtππ<\p~YP0y2H2|2v\64s )ed in
the attached reprinps and pIKaeS9if\@↓⊃KeJ↓o@∃β≤¬ε∞fDWGεL≥⊗rε
x
d∞~~4aQ]{tMP34z≤β together.  Our londεAeC9KJAO=CXASLABAaβ∪?∂K∞iβS#∂!β∂πp∧ε⊗*∞Mvf Q(f∞∨N4ε∞⊗|P≥∧∞~→(∞⎇|[→∧9Y⊂_pw⊂*\p¬ them e→MKGi%mKIr↓iP≥β∞≠#'↔4∧Rπ&QPV>|≥G4~=⊂~yP3t]2w↔εBαSometiee@LAShAβ;'31π+O*∞Mε*εl≤7'~M↔⊗.>MGJεn-vjε≡N2ε&≡L∩ε⊗≡8	$∞αytg→FE22Y:qz4]2P0w→⊂4w2≥qz4{→P897Xp¬ss@∃`
β3L[∃βSF)β∪↔'+∂S'4∧Rππ-xλl↑|y4aQ[yH
\=~→-\=~0⊃Xv⊂6'Yβic.A⊃←o∃mKdX↓o@∃β∂∪∃βπ`ε&.∞O∀π∨/,UBαDβ8pl≡]~≡$ε.-`≠XTVεE≥40z conjEctural proc`ggα+@~π⎇_
D_Y(
l99→,D≥~_.D→{h,>;{LD→→1∞\⎇~0↔[∧¬
as pre@∃]iYr↓G←]Gα+'[↔"q↓αO|¬V/&≥\W
ε≤@π>NMDπ/≡Tλ

<y(@0qz9H:7P #ompi1J~)⊗+cC↔↔!βCK|;@⊗∞↑4"π&≡Bπ<y(∞M→<p∩H30q@tpεAS\αβ¬β7|ε&*ε\`	M≤z90↔≥⊂;p|H:40wβE9tf\4∧e @IKCg←αs';≥p↓α#?>+[↔IbβS#∃∧∧WGε↑.Bππ-|w,;<h∞];≠λ
=Y(∞MβP22Y2yεE≥5P92Xyww4[3P;t→w⊂:g→|82q]2r⊂:\p¬ o↓_AQJAα3π∂S,∧⊗bεL≡F
@8X<lT~<h∞,<=0∀\2r↔εB∧E∧kYP27P≠5z⊂8≤5x7yYP:7P~vx6 %meft↓gkGPαβ¬βC⊗{↔Kπh∧εNnβ91
≤=→0⊗≡P⊂
maybe n`∨hαβπQβ∞c1β←LεFFNd

(≠Y/∞λ→P∀]2P<`%ars.A)QSβ→β'Mε∪↔∂π,ε6*ε≡N0hW>Xλl<αyyP→2x2`.ds on sucCessful fo@I[CYSiCiS←8AP∨→∧f∞∨N4ε∞⊗}P≥∧∞~→(∞⎇|[⊃¬A Uy$
_=P∩H6pr2H897c\2yyP~w⊂:4~yP3 /rhCYαKkπSL¬vrb.W"π|Tεn∂∀&*ε|8λn↑~91↓Q]z0~~⊂4p∀exclUpπSmKαceβ≠x∞"π&Tε6@|\p∩Ypq6 % future.  In short We wi@1X~+.kC#π≤¬↔V*∞Mε.␈,X

≤x;λ≡]~0∪~qtpvλ4w:2[64sr[1rP %xcepPAM@?⊂∧π&FTλ
m}X¬FE≥tz4 proo_[GQKα≠//.4π&z,Rε&↑8λn-8Y9∧Y;⊂↔]U

λ	The main areapεA←L↓←kdAAeKmSα{WMβ∞≠∂?7∧¬FO≡
\Vwλ_;LD→]0~≥y2P 7orc
are ↓QQJAMα{33?>K;≥↓F@~εmx
d∞y93E↔@εEεB↔4z2[oP⊂⊂
λ
∀F8A∪↔4∧Vf␈
\Vwλ≠qD∧,Xp∀\αcumscri` β#'?9+	βπMε	β'?&)β/→∧ε&.∂=yfNvt⊗v"
≡G_h,≡πεf≤<↔&N⎇`λ∞Mh_<NM9Z0⊃Zpr⊂ )np	KXαc'>]l6*@Hλ	&(z<Xn]<xp→~x:4`/n!1 Forealizes
λthe proc@∃`∂Mβ|1β∂?v≠3@.M≥f*αα≠p∪≥2p∞ Incorrectly) that a @
KeiC%\AG←1YKGi%←\~∃α{⊃β≠∞≠SMβO→βπ3bβS#π ∧ε∂⊗T≤L]→=P-nα⊂3'\⊂9wf≥4p∞g↓BAae=EP∪↔hq↓α' ∧ε&@y<h∞M~8	FBαby allowing one to fh∂e[¬YY`%ε@∨∨]\Rπ&≡Bπ&Tε.wM~FO&≤↑2π&≡Bε∂,Tε>.l↑&∂&\APF↔∀∞7ε.=≤fN.D∞π⊗↑<↑7≡∂4↔⊗*≥FbπMRε.nM↔&N↑4ε}H_(∞>→8z,m99λ
=;YAQU~~.4~<h={;;md~;@
∞98;D∞Y8<m⎇Z;Yd;Yβ∧[|@∞,8<smnh→→.<|Z8L\λ~;D∞~→(∞∞Y<⊂→~w:⊗εB1pw7]⊂12P_qqw`-plished by any fh∂eZαβ?2LV'.>M⊗}raQ h∩5`λλL=Y0⊗≠x6rw≥⊂7s⊂≥92pz~w3P![w1rx≥9P0yH4πbj@∃Gif\α↓αS#M→1β∪/≠∂K'⊗+⊃β'ph ∩Dβ8pl≡]~≡$ε.-`≠X∀VεE→αaci@1SiCi∃fP⊃β∞s⊃β7∂Iβ∃ε&/∂]~&."iw∩b∞,V∂≡⎇m⊗v:≤&␈/D
6v←⎇H	,Ly+λ,;~9,eβ"]l≥]≤k∧∞≠x|m≤Z;⊂∀]<P0w→⊂72qYyytz≡W

#. The current biggest gap in computer reasOningabout the physIcal @]←eYH4∃SfAβ##∃β≤¬voεLX
T≠_8m4≠yH∀≤}4nL;(⊃M}H≤Y,≡{{Z-lh_8M}=λ⊂⊃[w1z`2rent↓ae←G∃`∂O↔~p4*πd¬Bπ&Tε∨/.,Vwα∞λM|[→;$∞{{≥M≥Yh≤∞-βsy0[yP0y\zp
e that↓KCGP↓CGiSα{9β?2βS#∀hSCK??∪π5β∧ε&}≥8q.P0P .ext state that↓IKaKαs∪Mβ}qβS#*β∂WK⊗+;@"∞0
≡→+λ∞M→(⊂,>~;sE@ε@
and sometimepεA←\αβ¬βK∞s∪?Tλ
L≡X88ML+Hλ
M→>(Mxπ∪zλ8∧ake into accOunt @
←]iS9k←kf4⊃ae←α≠↔OO/→β ?$λ

(→P⊂Xz⊂:4_z⊂7@4her @¬GiS←9`
βπv!β↔[,¬g'~
\↔Jε,Tπ&∞αz3L@P860XrWεE∃p¬ believ@∀AiQCPAGSe
k[gGβ∪'CSL¬vrε\∨∩ε⊗Tλ
-↑≠|]≥]λ⊂∀[⊂37@2malizing @]QCh~)aK@?
F*ε=mw 4_8[n↑λ≤p~Xt⊂8roces@MKf@8hP4R5`λ
p¬ also p@1C\Agα{7*∞0≥∞\≤∧P /d∧AiQ∀AiQKα{@↔J
p→D∞_=≥↑[\k∧<|⊂∩Xβial1rAQS≥QKd~)←eIJπ⊃βCπ'#↔K;~β')β>C'∂!g.v>M⊗}R∞hλ.
88[↑h≠8/∀_Y(
\=_p∀→p∧ and re@1CiS↑αsL4⊗+S@>\XD∞_=≥↑[\h¬T→[`9λ2|0v\4∧e, the ↓IKYCi%←TAE∃i`∨↔(¬bε
∞λλ.Nα2y7λ22y`#p¬SESαs∀4,⊂λ∞O<→(
|β⊂:4≤2rVr~vrw9Zwp∞al h∂EUα+∂Qβ≤εV≡B≡2ε
∞λ	.9ww or a↓mK@#L∧6f*≥f"ε≡N0hW≡G&/-hd
βs⊂ )ts p@∃`∂↔∞FN}βH$∞⎇8z∧<h⊂∀]9P8rojec↓QS←LAα{9β¬∞&/&≥l∩ε∂4
V}&≤h
,\β"P⊃≡P0w3[2P7@f r`∪gαK?91∧c'∨#&K;≥β∞s⊃β?≤∧6G<z0↔[⊂1<P≠z42`2 h∂EUα+∂SMph ⊂HαB2-d_;⊗λ:44`3 w`∨e,XAiQ∀AK@7∧¬ε∂≡≤4εO~
ybπ⊗↑≤L↑y;]≡~;p↔λ0πf QQJARαs∪ ?-\↔&N⎇aP@.~_=∧
<h⊂,>≥8;
O(_=L≥8ε0q≠2P:7H0s⊂ /bserver with give`≤Aα{CC?↔#W;≡M⊗/~∞Mph⊗|.6/↔lTε∞vDλλm⎇<≥0~→W

λ
)v≠	αC⊗{?2λ=ε.≡=≥f 4_↑(λ={<∃.L<C"APB5y$
αzy@4 dis@QS]OKαK@≡B∞Mε.␈,]Rππ-}fNvt'Jε=x.∞αz2`2 from pro@=L[GQ∃GWS]≤~∃Er↓G←[aUiKd\4⊂∩∧∪%hASf↓C\AKβ≠O.nM⊗∞b∞λ↔↔λ≠`∪λ:42P≠4πti@=\A←L↓ae←↑ε1β'9ε	β≠}-V∞`Q.7O∨L]Rπ&≡Bε
8λ-l~9_.L(≤→≠ws⊂ #an be che@
W@↔⊃ε∪eβ¬∧¬V.≡≥fN≡≥Dππ⊗|8	.yP∞
It is a c@=]gKcUK]GJ↓←@→β&C∃β←|ε&@4≠yHλ⎇y9→-Eλ⊂r∞↑Xz≥Yλ∃∞↑X;Yd∞~_=↓QXπ7P≠p¬chanical pro@
KgfAα≠π9β∞c←πg~β∪↔S,ε&nNβY(∞⎇→=~↑H_ ⊂≤97w@& h∂LA∧~∃OSYK\Agα+;@&]l6*ε←
↔∨'4λ
-d_(3≠y6pvλ9xy`4em.
In p@IS]GSAYJXAQQKeK→←eJX↓ae←←α17∂#.≠/';8βO#?,c⊃β*β↔πOJaβ←#Lc∃βπd`4+SF)β∪'4∧fN∨]NFN∂4	v2π]lF/↔>L⊗v&≥lrπ&Tε∨⊗\≡FO6T∞π⊗↑<Z7≡<h≠lD_#"M\=~→-\=~0⊃Zpw⊂0\2P4w≥7v; %d in↓[CWS9JABA!SOPAA←oKe∃HAiQ∃←eKZ↓ae←m∃d\
∀4∀∪⊃←]KmKdαaβ'9π≠C'S*β?2∞Mε*π=≥Wεf≤9↔'J
x	D
;y→.-β⊂67Ytqpvλ0w2 s`h~)iQK↑β∪↔S'~βOgO&+7Mβ∞s⊃βSF)βK/3'S@∀λ
m≡~λ⊂≠Z4qt⊂≥42|P≤2y6t]⊂0|4[vpz4↑4p∞g
mathematicad @¬]HAa!sgSG¬XAgsβ≠S↔7~aβ∂#,≠''≠8∧ε∞∨NX⊗bπ∞-v}\c"M<h⊃-l{⎇;NL<Y9∧Xπy6Zp∧able difdicu@1iSKf8@A∪h↓SfAK¬crAK9←kOPαβS=βn/∀4WβK??2k∂#↔≡[↔KM∧3?Iβ&C∃β≠␈∪7π1¬≠gOS.k@~ε≥dεf↑⎇_2ε∞l@π≡∂Dλ

8πy<H8∧extbooks,
and we have done it.  The difficulty is that the formal proofs of easy
theoRems turn out to be Ten timas Longer than informal proofs, and the
excess in length grows the further one advances into the theory.  The
αtroublE is That mathematicians have not succeeded in completely formalizing
the languages and reasoning pRocesses they actually use.  Much reasoning
that at first seems to be within a given mathematical system, actually is
metamathematical reasoning about the system.  Even when a mathematician
is working within a system, he establishes shortcuts whose repeated use
keeps down the length of a proof.

	We havE a pRoof-checker called FOL (for first order logic) (Weyhrauch
1977a), we have been improving it since 1973, and we propose to improve
it further under this grant.  (Rewriting it from scratch will be required
at some point, but we aren't sure when this will be the best use of
limited manpower).  With FOL, we have Checked a varieTy of mathematical
proofs, and each such pro@)KGhA!CfAi=YHAkLAg←[∃iQS]≤ACE←UhAQ←\Ai↑A%[ae←YJ~∃i!JAae=←L[G!KGWKHA←dA!←nAi<AM←e5CYSu∀ABAO%mK\A5CiQK5CiSG¬XAI←5CS\A=d~∃Q=nAi↑↓oeSi∀AC]H↓IKEk≤Aae←=If\@↓)QJAAe←←MLAIKg
eSEK⊂AEKY=n~∃K¬GPAi∃giKH↓iQJA¬ICck¬GrA←α1α~>bβπ;⊃ε{WIβ∂C'?7∂#'kπ&K?;Mph(4	F	%απwIβ∪↔4¬⊗≡(_x.8[⊃$
βs⊂0Xqrx 4ing general mathe`≠Cr of a su@	OeOk@AWLA∧AOe←U`A∞A⊃SmSI∃bAiQ∀A←eI∃d@~∃=LA∞vααKπ7≤+e∨M∧εFF.β|Y-WH≠⊃.D⊃h_LT_(_m};]_,-≡(∩-lZ;Z.L(≤q.D≠yH∞
z;]∞5λ→8,=λβ"N
z;]∧Y:;LT_{sMl8⎇→,D≥≠h↑Y<↑$
⎇~→.$_↑(∀≥~≤L\9λ\8zλ∞M≤Y8,D_Y0∀[3P92Y⊂7p∩
bdack(@AQQK\AQQKeJ↓SfAC8ASMM%]SiJ↓gkEg∃hA←L↓iQKgα)βC?LsSMβ≥+∂!β&CπQβ&C∃4T∧6}vlXλnM;Y`∞M≤Y8,Nh≥z.M~;@⊂≥42P9]q9r`4 are all of the same colOr.P~~(~∀QF$A/SYM←\Of↓iQK←β∪↔5β&CπQ↓∀K→βA∧K@~π∞-⊗n(≥~]H
≤¬V*((
<h≥
(≤Y-\:;Y↑H≤&∀β"Um;H→
≡Z9→,D_↑(∞∧H~<d(≤≥.,;≡(≡Z=~
\=~0⊃H9z0z→vrw:⊂1:`4 its proof uses a 
pairing argument (requaring sEt theory) which is beyond the capability of 
present Thegrem(ae=mS]N↓ae←OIC[f\@~∀~(QH@%¬;∃β∂F+∂/↔"βS#∃ε3'KO ∧ε}vT
π.vN,V"πMV␈⊗]↑2ε↑d∞6/"∞Mε.␈/∀ε∂~∞λL↑y;]\λβ"M≥H∩q)I⊃66eeW+@∧
~~<d∞x<hm|H≥
(≤≥..≠|y$
yH→.>_8[
≡z~;Lt_(∪≡Yy(={≠→,>~;{AQ[yH∞∞[{yN4≥≠h,(≥<l\λ_<dY;Xm
8<Zn4≥≠h
\8<⎇.,(≠_.L<H~,L8<kD∧β"C!%→*(
M→(≤∞-x[→-T≠yHm|[8-M>Z;Lt~≠⎇d∞y(_l≥H≤Y,≡{{H≤[⎇=∧∞z_=∧
⎇~→.$≤→;n
→(~mm⎇c"N|<h~-M≥<⎇∞,=→9∧↑(_/
;{8.M>Z;Lt≥~→$∞z<y$
8;H∞∞[x[]6s8djx=≠kUHλ∪ml(≠yD∞~→(↓QZ_<LD≤≤[l-→;<d
→<Y$∞x<h∞Mh→[n-=;_.L(_;LD≤≤[nl(≥~≡λ≤{m\(→;∞<(→≠l↑{I⎇∧
{[⎇aQ\{{,↑~~;LuHλ∃

<h≤∞-x[→-T≥x<d;≤{d>~;m\=~>L\λ~;D∞y8{mlλ≥x/∀_↑(λ=≤Z<dλ{x9¬a"C"EJ(∃lT≤≤[nl9λ≥
(_{n.Y8⎇
l<|h
|H≥~T∪8pl≡]~≡%Z_:;NL<H_m⎇<~;↑Vs8dn_:;NL<W+AQU~~.4_;≠
}y9λ∞↑h≥≠d{{<≡Y(≥
(≠|M≤z;X-D→Z<N>λ≠|LL<H≤∞-{yH∞⎇=~λ∞={9#!-;|Y$∞Y8y-nλ≤≤M⎇y\vn.⎇i\L⎇+_[o≤<I[-⎇|Y7!QC"B*,8y;ND~;<∞-⎇Y;,]]≤h
=Y(∞,9≥8l\λ≥~T≠→;L}~λ≠ld≤{{,T≤≤[m|\h_O⊃"X(l8⎇≠n$≠yH,=≥→.$≥~_-d≥→;Edλ∩→.,(_<LT≤{{,T≠yH∞M→;(≥Yλ≥m=λ≥
>(~≡Y#"L≤x{{.
~<z\C"AQB09NL<H_$∞→<Z-|λ≠yD9→~-lh≠Y.t→Y8.N<Y<d∞≠h⊃Iyλ≥y$
_=Q$9x:-d_Y9n]H≥≠d↓"Y6∞<Z;,]]λ∃m≡~λ≤∞-{y\d;Y
}<H~-m=~8-D≤⎇0⊃Xp¬ss@∃bACe∀AK@;≤{WKπ>K;≥9ααS#↔≤∧PhW,\6.wD
⊗oπ-}f.n]nG~ε≡f*π,\G.≡\Dπ&FT
F.v}Mαε}d∞6}nQQ'π⊗⎇|g~ε/∀ε
εl≤7&␈$
v2ε,↑G&/$∞FF∞d
F.rd∧¬&FT∞&.'\=⊗v:∞Mε*εL]f?&∞4ε}H≤⊂→≠ws9FB27ryH77z_<P4z≤rv3⊂≠rpw⊂≥40z wa are gettinganywhere.
λSome kf The pI←←Mf↓o@∃β∂∪∃β;|εrππ-xG.≡≥lrε∂,Tε∞⊗}P≥∧<h⊂⊗≠w3P0\F@
their @%]M@?⊗kπ1β4∧W.z;p↔≤Tε  This IpεA[←MhAGYα+πKM∀ε/6α9→-nα⊂4`.
the !2c@¬[KMe%]OJJDAKqC5aP∪∃∧∪↔3>8q↓αP≤LT_<Y$∞~≤Y,T≠yH
}<H⊂→→qrw:βE2|(→y4vr[89@~
λ
∀∪→SY[C90
9:h∧εF∂4
W≡∞Dλd|@λ≥≠d∞z≠p≠H:40zλ:42P≤2py`/ni`≥Nαβ';[|¬G6.D	⊗rπMRhα\p↔[8¬ti@=\A←L↓BAQCIHAeKβ#@⊗␈>λ	,>~9Q$z→<nP897X4∧em↓GC\A	JAM←I[CISiKHAS8AM@'↔≠P4-xLL<H⊂⊗≠stqWβE+rP_t7qbH:44iH2|0v\4∧e @→`?5∧¬w/'=≤F*ε\≡FF.β8=
≤|kλ,8x=.<αP4:[pw⊂2easo@9S]N~)←@≠S,qβ7πF+Eβ∪,∧G.∨M_md≥z0~~⊂7q9Yy;0z~ws⊂'Yα the kutsi`	JAβ;?K3 ¬Bε∞l@λ
|\y0→≥0z4`/nλ
∃↑α1β¬β≤C↔OMα)KCπ↔#'π⊃∧εε␈≡≡M⊗}rV⊂λ
≡h≤→≠vtw2[8∧ in thi@LAKqC5aP∪∃ph*S#*βO.β8;NM8c"L≡≥_8m
9;]∧
98r≥X∧y`- h∂LA→∨⊂⊃β>@~π↑8	,D≥≠h.8;→∧(≤p∀[zpation @=H	β#M→β∂#/≠@~π⎇xML	Hλ	 εE #ouldthen↓kgJ@β##∃β≤∧Vn∞nM⊗~π=≥Wεf≤i⊗≡∂M_md≤[u.M9Y4d
βs⊂#∪d∧ to ans@]Kd@Q%\AB~)gSMO1JAgi∃`RAcUKgiSα{;MβfK/*∧-↔~εTε⊗@_8zd
z;Yd
;H⊂⊃Z2qu@≠w⊂17Xy2⊂!λ⊂10→
looking at hiS model, rather↓iQC\αβ∪↔∪,∧6Nvtgε}Tλ↔FN⎇↑2ε∞-zW"πMRπ↔]H	.∀≠yC!1t2y\β that black wapεAS\αβ∂#↔≡Y9↓α&C'Mβ≤¬⊗v>LTπ/≡T	v"π<]V∞wM_λd=≥_,=≠9;NA ¬9`]2yP9Y{2y0[⊂4:w→2y2rλ9z2x≤β o`-∃`Aie¬ISiS=]CXAα3?K↔∞c'kπ&K?;Mph*≠πfkπ9∨~βCK?x∧bεO4∞7&NMDεo.=∧εf}l|W∩πM⊗rπMRεNlhn-8;λ∞∞[{`∪εE1t≠{tw3H:40zλ9rP9]4v6⊂→7w∪zλ3:v&≡P:w2→y9z0[2⊂47]P4:vXw9P #ombine observation
with↓IKIk
iS←\8~∀
∀%/@∃βF[∃β∧ε&.f≥]⊗v∂/∀ε/∨M≥V∂&↑4ε}H≥~T≠→;L}~λ∪lD≥~→!QRy3
L>(≤l↑λ≥~]|↑(∞∞[{yNP6rw≥4ww2Y⊂0q7]2W⊂⊂∩w⊂0wλ4p∞i@QSCHAα+cC↔⊗K7π; h+@/=≥f 4≠{[∂∀≤_<ND≠yH∞M→(⊂n↑\Y;NM≤∧P0]0tv0X4∧e @→KCikβ∪↔M1∧εv*π,\G.≡\@λ∞M→(≠N]8Y0→βE7s⊂≤z2x9H72qr\βsary to prove the @→SeghαβS#'↔#eβSG∪↔*∞Mε.␈,YW
εn-vjβFf∩π&tε∪β"βC"H={\p∀Y2y4w→β that id tace@LA←MJ↓giK`↓U`↔O ∧π&ZX∞∞∞Y<p→H:42P≥42w`2em, @QQSfA%f~+∂+'S∃∧K7CK/≠@≡OlUbα¬|Tε/G\7"πM↔"ε≤LFNvt∞FF*⎇v∞b↑8
∞.8⎇≥.,(→Q,≡≥<Y.4≠9;NM;{Y,A XY-M⎇h⊂≠Zv6⊂9]q9z0[:4pv≠<P92Y:qrP≥42y`% prood∧AYK9OiQf8~∀4PJ'9β≤¬vvV\8

≥{H⊂≠Zz4⊂&Xapy:~<SyP≤2qrw≥⊂∀⊂\M[P	 @→←e[C1SuCi%←\A←α04*2M~AβC⊗{∨Kπo→β@/=≥f 4≤y;NL8π1`%pεAC]⊂AgGQ∃[CiBαβ?2m↔↔∨D
w⊗&↑ λ
Mβst`#, we
hav@∀AGQKα≠/.D∩∧4yDππ⊗⎇p	D
βs⊂ 4he c@=`K↔≥#;↔O~β?2

↔4	,\l≥99P→~w3rRLF@
pI←@∨K∞i0⊂hαI,N<8εr@fp¬S@;>*`∨BLε7$V(~0→CE::`2ns tru`
ASα1βS#*αM'↔GβK↔O≤¬⊗}w4αgBε≥lB↓7∀
ε∂6T≥
(≤p-\(_=
⎇<c"M≥H≥~T≤x;,T≠|Y↑KHλ
M~<h∞∞[{`∪λ0yP #hecked by FO@_Aβ;πMβ|1βS#*βOπ\Tεf.βY⎇
↓ X<d(≥|M≡≥→;D
⎇=⊂~w37i≠pr⊂(≤7ws⊂≠pε the same result. We believe that su@
P~¬M¬m←eC	YJAe∃gk@3'→βπK*β∨π≠/∪π33JβC?O≤¬⊗⊗@→+C!!"B3n↑H≤⊂⊗_w9P#≠y⊂#'S⊂4w1[8r2P≥42P#≠v67`7ing:

α(DRA)Q∀AmKe%MSGCQS←\A=H	βSF)β∂?↔∪↔∂Sv+OMβ|∧b∧d~:αππ-xwε∞↑5bα∧-⎇εpHαS8@Ppy:4≡mP∞.]  has recently begen pgS9H
βπFK?5β≤∧6F.β8<d∞≠h≤∞-⎇Y(∞M→#"N∞[|⊃.∞~9<d
βs⊂&∩ih⊂8≤7sy0[yW⊂⊂∃p¬ inte`≥H↓i↑AKaaC]H↓iQSf↓o←eV↓ErAS9ie←IUGS]N4∃[Ki∧[[Ci!K[Ci%GCXA5CGQS9KerA%]i↑A→∨_@QMKJAE∃Y←nR8@A)Q%fAoS1XAEJ↓M←YY=oKH~)ErAB↓[CU←HAKMM=ehAi<AkgJ↓≠GπCIiQbOLACqS=[CiSiCiS←8AP∨→∧b&NAε;⊃β&yβCK␈3∀4∧ε&␈ε↑.FN<h≠l@⊂9tv\4∧e LISP prkgrams&  Wayhrauchhas @IKGK]QYbAaα{';S.!β?W h#S#∂!βS#M→βOπn)β@&\=εvO≡X	$x;@⊂_2P:iYr⊂:7H30∂rmulate part h∂LA⊃C]BAMG←ih≥f~∃Gα{'CW&S'?p∧εNvNX7&N⎇`λ
≥]≠hM<\p~λ5y22\⊂67`'ic.  This also requ@%eKfAβ##∀Q(,↑_;8.M→;8.M8x;∧
88z
≥Y<↑%Dλ∃y$>≤⊂∩Xz⊂:4~yP:7H12P)\s34`#iaftly practic@¬X∩+4¬w$≥<h∞MβP:`3e thhpεACq%←[Ci%uCiSα{9β'p∧¬∨&≥lfo⊗D	DM≥∧λλm}<\p∩\β 4Ph ∩C%∀∧∞vβ⎇~↑H_<n8⎇⊂≠pε p↓I←@∨K∞iβ@6↑-⊗&N<≡FN}dλλ.,(≥z≡λ_<LT_x;
L9λ⊂∀[8∧ensio`≥C0@∩+αλM}→<]
≤αyP /d∧Aae=H∂Kπlε2`$λλ∃
<y(
≥X{≥,L(≥~
≥Y|h
M8¬rP~5{P&]qt⊂ 3tkrage a
program u@MKfXAα;⊃βF{Uβ7∞seβO&+CMβH∞Bπ_:y.4π⊂⊂*~2yrP≤zry@tions ca`≥]=hAEJ~¬CGα[↔"/∩ε∨↑.&.wDλ	M↑Xεpv~yvyP→4πr MatheMatic@¬XAiQ∃←erAα{⊂∩ε=x.∞αz0z~ww↔  The
λrequire ↓QQK@?⊗K↔Mβ&CπQβ≤¬vw_:3D∞≤[p∪\αaes as objects afD↓CC@9εF∞f4λλ,-βzzεBαthe abstract pp¬WaKβ∪S'↔~β?2∞Mε*ε\≤6FNβY0→H:40zλ:42lH9:w on ≤@↓≠←ghαβCK↔0
⊗␈/4↓PV6β|[,≥λ→0∪→4πrts hav@∀A←@;eIβO#|εvrπ∞-wε/.M⊗/~
p	D∞~→(≥→{`9~z46`3 cgmPuted↓Ab@~)ae@??∪π7M`β; ?D
π-βx2`2ties o`A`π∪??,≥W4≥~→-↑y;⊂≠→yW⊂→⎇Y(⊂∩↑1rxtio`≤Aβ;πMβ$C∀4.⎇gεZ
p	Dλ8∧r@llo _A0\XAβ%KYY↑0A~\X↓(∂/≥
&∂.9∧
Tk@↔↔T∧ oN PASCAHλ@9ααS#'α4π <8	FE_βarrie`λA←β+QβW≤¬⊗v~≥fo&XDXπy6Xv⊂9`9steMand @]JAQCYJAU@-≠Qβ,;W9β&yβS#Ls ~Q(λ,-βzz<zqt pr`∨E1K[fAU`∂'lpλ@4y1`4 h∂eI⊃dAY←α;'
aQ hR∧5∩¬&Tπ6/-⊂	M≤x=∩-⎇H≠`3λ:42P_wy92Xz72y\β of hardvare @
SeGkαKQβ∪,ε6N>d
W=8π3@ 
∃
∨0AG←]QS]kSαs~πMRπ>}-2ε@yH∃l≤yY0→⊗W↔&@.  Almost All p@IKgK]PAQCe⊃h∂πK(h#@6↑-⊗6N<≡FN}dλ
.P10yYp⊂7gβE9tf]v0z4[3P4`4 if all p@=`∂'d∧Rπ∨L≡F/~d∧¬.∞⎇lW∩εL]V}w>N&∂&\APG&≡Bε6β|[,≥λ≤→≠ws9P≥40z=42P$_y2;p\2P4iH1wy9→qz⊂0\2P3 %asible and
re@EkSeJ↓YKgf↓Qk@7∞qβπ≠ ∧ε≡}↑λ
↑H≥{n-h≥~≥H≥~T≤z;.]_=~-⎇H≥→,=≠Z<.\αyWλ+rFE≤97x7\p¬ to continue this work.
¬
(4) We intend to redo the theoRems of KeLley mentioned above using
the many newfeatures That have been added  of the metamathematics, axiom schemas
useful in proving the correctness of LISP programs.  Another application
of schemas is to axiomatizing circumscription.

(6) The usefulness of the metamathematics will be enhanced by our addition
of certain reflection principles.  ThesE are rules that state some relation
between a theory and its metamathematics.  For example, if
you hav@∀Aae←YKHAB↓GKei¬S\AM=e[kY∧XAiQ∃\AS\↓iQJA5KiB[QQKOedAs←j↓GC\A¬ggKeP~∃iQ¬hAiQ∀AM←e5kYBA%bAae=mCEY∀\@Aπ=]mKeMKY`%bβ';≠␈∪7π1εkπS#.kπS'∨→β/≠&+9βW≤∧W_h-\W&∞\≡FF.β8=
≤x;λ≡|y0→≥4ww9H:40zλ0v6⊂→4πrmulas @]SiPAα≠↔KS∞K9βC⊗{C↔K&K↔Mβ∂∪∀4.N'.*d∧¬&FTλ↔'_8p∀≠pp∞t↓[CGQ¬]SgZαβ∂?↔⊗K;↔⊃∧εvO&∧≤L\β0e@
iSO\αβCK≥l6OεLXaQ]z0⊗≠⊂0vlow u@LAi↑AαWS?nS'∂∞c3@J∞XlT≤⎇0⊃Z⊂6r`4atheOrees
λ¬i↑AA` ?lTπ&F]p≤L]<h⊂∀[⊂:42H10y`% the@=`e8hP.cb↓!Kegα{; 6]AP@@ TZ,t0y2λ+r|`(p¬CkGαAβ'M∞FF*
\⊗N@H→→.tsw2\⊂0w2λ4rxlementer o↓_A
∂_8@A)Q!`
βK,ε↔.O,XaQX(∪≥v6⊂*[22y9\0p∞ding o_AE@?αMαε@8πr2\0ε mathematical logic(λA`β∪??,≥VnNβYc!∞α2q@hliqe@∃`
βπv!βS#*βπ≥H
.N(≥≠d≠h⊂∪[wr⊂(uman↓KUOSαs↔/-_L@Pε~∀4∃)QJ↓
∨1∞π-zY0⊃\⊂0z:≤αacts cgnSi`	Ke¬E@∪∃¬⊗w→<Y∞>λ→@→≠vP<`/ung Mathe@5CiSGαKπ;↓1Q'.Ft
m}8ε2;4pe, f`∪]¬YY`%bβSz∞0→,T_{p⊗\8¬te@I`
βπα
M91≡LβP6`]42vp]4qpvλ92y`%arch
λ¬S@9∧∧∩π≡≤⎇fNX∧q`!npλAo¬r@→↓∧	βK|L↔&NβQ`≡,<q0⊂\αch @¬`∂O|8
,≡→<`∀~x⊂;d[4∧ benefiPAE@?αMhW∞-v}∩\8
\zz;LP92`3earc@ ~∃C]⊂AaQJ↓ae@?αλλ,@pz4`/n of its @IKgkYβ#@~Pβ"C!%Xp@⊂⊂αi`∨OICaQr↓←@→αT¬vF↓H∪8@Pβarthy
∀~(X↔>K9β;x¬'∂∨G0λ
≥Y→0↔≥⊂_⊗
∞F@
BORN0∀@↓'@↔C↔⊂∧β"b ≤L≠P4gλ!0∂`'Q←\@1∧kπOO∞≠#@/<P
∞Na"C! ¬DEBAP@∪∨8pλ (%h∞,9X8lT≥@8y192Xu]FE⊂↔)W   @≠CQQK@7∂#'∂MJα≡∞β~ 3≠βr`≥Sα	αNn0≥
≡≥=→$βs⊂*→qt77[4πgi 194`XλhαT⊂∀
α@λ@9αB7πSF+7πSL∧'5(∀9~tεce@Q←P→ααXM≡Y<\m≡≤∧V⊂\ZP@.
.s@-S`~∃!_∞ 4z*2∧h@λ
9βadbU$bi]β@
Amep¬SGC8A≠Ci!K[CI%CC@1¬≠?∂'(∞GJ`Q(↔>yxp∀Xz4w`. f`∨Dβ∂?7∧εW&NβY`⊂∪pqt4[2y<FβE)t`'ma Xi,~*_¬Fn∞βH⊃L]≠≠`≠H4p∞ Physi@	CXA≤∧6N8π1`% (19T`
 +W∃∩`HαP0iT⊂π0z~wp∞al Lec↓Q`↔K↔⊂¬!E@⊗f∩J@Q)∀,,UAP@(+S ↔λ*:y4[1P {↓ard ↓→`/Tλ↔>yxp∀Xz4w`. f`∨Dβ∂?↔∧εW&NβY`⊂∪pqt4[2y<@
_X	7DRD4Rs@≡↑_β!( ∩OFESSIOLAL EXPE@%!~∞+P4*C⊗{∂S?α λλl8ε6/w(λAβ∪' 6<X

⎇β⊂ ∃@9SmKeMSi`%αAEeUαiUE$`h ∀F≤|vNw4
&/≡\≡&≡B	_N>≤Y0⊃]4πr @%\A7∂##↔\≡FN∨5D¬π⊗≥l6/&⎇`λ
]X∧{ %p¬gSid@Pbrβ)E5U~I04(≤7&NβY`⊂⊂yyti]0s: Prgf@∃`∂O?⊂∧ε}H∪8.M→;8.M8|k∧
⎇_;L@7y2 Un`∪mα+@↔≡≡O∩αC↔⊂
&5αZZTKε@
AspπSgi¬]`⊃α∧ε&}Y<p→[y⊂7@f Mathematics _A⊃Cei[=kiPA
←YYK≥J@P@	IUU5+A%04T@∨≡≤∧p~_w:⊂(≤4πfesskr od∧Aπ←5[k@;L∧6∂&≥yb¬≡=_Vv≡UD∧jt∃jBbα∧⊂∞&W)L%∃β"P.ywq`)ate Prh∂MKMgWdA=LAπ←5[k@;L∧6∂&≥yb¬≡=_	-ly+λ	UR+U¬dλλ&&@_V[→
VεE(≤4πfeSsh∂dA=H	α∂}kC@/LXD
xz1-ly(∀n8π3 /rd ENiversitp∩@ brldα↓5βC⊗+O.n@
%A ¬↔9Zβip
PROFESS@∪∨9β_A∀*NByj4L∀→I∃$LZ4∧@Qλ∀h913U	_R0h	→U⊃4HZu∀nAQKXtN≡_8q'1"Uz.Mλ∪8..X∧w Minsky organaz@∃HAC]⊂AISe∃GiKHαβS#∃∧KS'4K∂'πbα';S.c3'∨.s∂∀∀UβK?+,≠Qβπ ∧∧jt∃jBph!Q$␈⊗|≥fOV\Dε∞vDFO⊗\>G
¬>L⊗v6},B∧∂.M⊗6N=≤⊗b∧≥nF.fM≤v.v<T¬π⊗⎇(V∨ Q!PT→=P∩[7x2rλ:42P∪$ih⊂≤97sy_vp
indεAgsβ≠S↔∃∧3?Iβ≤¬voπ↑M⊗v:∞⎇↔&@Q.7Nn-x
≤h→>∞∞Y<tm≥{\k∧∞_<]
≤z8λ0]2r⊂$[⊂:42H22{ %lopment
of the ALGOL 58↓C]HAQQJAβ1∂∨_@X`AYC9OkCO∃f\
∀4⊃!eKMK]hAMGSK]QSMSF↓o←eV↓SfAS8AiQJ↓MSKY⊃`
β?2απKSL3'∂'∞`4*'w#↔33N;↔;∂*aα∂?oβWSπ&K?9β>KS!α∨K7?fK
α↔GβK↔O≤¬⊗}w5APTn≡Mε.n≡M⊗≡∞βλ∃
8πy<H4πf Compu@QCiS←8XA)S5J['Q¬eSMNαβ∂?7π+S↔HhSOgO&+7M9h($*¬*
2&≤
R&>u→h4%l6␈.n@π⊗.d
⊗vf≥lSZε≡@λ∧"β⊃⊂λ≠2|:≤2s≥@
⊃-Q∪≤2s∪⊃↔P⊂⊃∀Nβ⊃¬
.  atDpD@@DBdDDvAChα↓	`2$αα∩+∀"∪Xh!Q!2∃Mx
l≡Y≤h∀∪8=
8εpz~qpv⊂∃42wi≡P7s⊂⊂wvx:]0z4w[⊃⊗⊂$[∧¬
<Prh∂F\↓∪
∪ ↓π←]OIKgf@Xd|XA9←eiP5⊃←YY¬]H@1∧7OS,ε&&∞UDβKf5`hPQ"b∀
λ,↔∞O4f␈∩⊂∧n∂MVn∂M≤6∞b
Mε.␈/∀ε}H⊂sm↑≥=_.M;{HEA Z;D
H⊂M≤9Y[n.λ_;LD⊃H	<\p∀_2y3P
2r9W
V⊂≡![vx:`4er P@I←OeC5[S]N↓C]H~)
←e[¬XA'sMiK[fxXA≥←β∪S!6F{3 &≥lBb∧≥↑7&/,L⊗jbε↔∪3~βC"AQEJ≥m≡~λ∀ed⊂[r-L;KλλUβ⊂#)→r5tw⊂!↔!K)↔⊂&~quv4Y2y∀FB⊃ P*~vrViZ0y4w→β Debu`∂OS9JA'sβ≠S↔∃ε3?Iβλ∧¬≡n≥H∧λ{{<∞↑→<HED∂∀⊂→≠qP∞
AFIPS Conf.8@QM∃πεR0A-←X8@dfXbrlf8~∀4Q1#←'&Aα→dλ6␈⊗,≡FzB	Ub∧_9yl↑≥
(∧*~→(	M8π5t[3FE)Ysvrw≥⊂)z`"program Language and Linking LmadeHA!e←≥`π]]⊗v8Q)F∞v|\⊗><h@⊗λ≡!wv[Tε ACM> _A)kY`%β	eYMph(4λ2∩CK?⊗c↔7M∧¬⊗rπMR¬&]w/(≠p∪λ!wvx≥z0z4[w⊃⊗⊂∂(97`#, @∪
% ~*≤¬vv?,↑74. ≠
←↔εEβE⊃*~vrViZ0y4w→β ComppiKβ⊃αOgα8
]<h@⊗λ4w⊂+K⊂ ∂rr (ed∞),
<Conv@∃agCi%←]CX↓π←[aUiKefxXA/Sαc↔e1β	eYYph 4"d$
∧mz&n∞βλ⊃↑x|Z.∞~;sD
βs⊂ H)zq9Yz⊂7@& Algol", @%\A(\4⊂
OS,∧Vf*¬V"r∃DβdXπy6Xv⊂&0[3zpsYP"2yXy0p⊂↓QS←@9∧cπ;∨αX⊗.<h⊂∪≠y⊂!`/iputdr~∃!β∪??,≥VnNβY`∨⊂ ∞o↓IiPK⊃9Y@3πv!1απm≠S↔K&5!ε⊂∞&FIC"AP¬⊃$[30∂rmatio8DX@@e≠≡N]nFNX∧qP⊂vry4Xβa`≤\αaαO↔∞F.n,P≤AQL. ≠
α.~∀4⊂λ@2(8m≡≥=→\α Contr`∨X↓←@→αλ∧∧F∞βY≤≥Yλ⊃/≤αQ⊗⊂~w⊂⊗(≤4πc.
ThiIHAβXεa6Gm⊂md⊂{{Ll<Y0↔_p¬ o@8Aβki=[CiSα→α∂?w#C >D¬¬&.=
fN≡≥AP@(|∧q2\4εetias!>0A≥C,[¬1αnp↔≡≡x¬`⊗λ_\[≠H∀)0∃@M`∂'πp¬∩`!α@

⊗(wiQPAλ≤↓K'∞q1α≥p∧∧6.β→≠,≥Hε⊂ [2⊂%↔λ pl∃\R@DQ⊃∨$@4ZAα~)	Sgaαcπeα⊗@≡9λ∃
≥9+4m<Z3L@P)|`3te`~Dαa↓`%∞-v~↓H⊂!I~∀h⊂m⎇YK@∨λ∀#%!↓A), Vol ≤~(f`@1¬##?↑λm⎇Kλ∃l≡z~0↔→z7w, @λ@:~q1↓EHεc 4β

λ∧ →#>CS!αT∧⊗n<h∀≥8π:2↓p∧R@D
[eeKα≠S 6↑8dπs⊂ ! C`∨[ββ'3↔⊂π⊂⊗@|C"H≡X∧p∀hi`iSα→απc∞&/∨=_m@9Qε⊂vry. Ma`) X	αO|∧2`%λλ∞(≤αh∂F\αα@∨Nβ<⊂↔\βia @%\4(≡πε@~90∩λ&pp∀h., M@¬iP@9∧@∨ε\0≥∞can Elsevier, New York, 1969.

⊗"The Home Information Terminal", <Man and Computer,
Proc. Int. Conf., Bordeaux, 1970>, S. Karger, New York, 1972.

.end
.onecol; cb Budget
.begin "budget" verbatim select 5;

PERIOD COVERED: 3 Years: 1 Jan. 1978 through 31 December 1980.

Dates:                1/1/78-12/31/78   1/1/79-12/31/79   1/1/80-12/31/80

A. SALARIES AND WAGES

   1.Senior Personnel:

     a.John McCarthy,      7,575.            8,181.           8,835.
       Professor
       Summer 75%
       Acad. Yr. 0%

   2.Other Personnel

     a.Research Associates

       (1)R.Weyhrauch     10,400.           11,232.          12,131.
          50% - 12 months
                                
       (2) ________,      17,000.           18,360.          19,829.
          100% - 12 months

     b. Student Research 
        Assistants
        (50% Acad.Yr.;
        100% Summer)

       (1)	           7,155.            7,704.           8,320.

       (2)                 7,155.            7,704.           8,320.

     c. Support Personnel

       (1)Secty(25%)       2,615.            2,824.           3,050.
    
       (2)Elec.Tech.(25%)  4,895.            5,287.           5,710.
                          _______           _______          _______

   Total Salaries & Wages 56,795.           61,292.          66,195.

B. STAFF BENEFITS         
   9/1/77-8/31/78:20.0%          
   9/1/78-8/31/79:20.8%
   9/1/79-8/31/80;21.6%                                          
   9/1/80-8/31/81;22.4%
                          11,510.           12,912.          14,475.
                          _______          ________         ________
C. TOTAL SALARIES, WAGES,
   AND STAFF BENEFITS     68,305.           74,204.          80,670.

.next page
D. PERMANENT EQUIPMENT        --                --               --

E. EXPENDABLE SUPPLIES     2,040.            2,040.           2,040.
   & EQUIPMENT(e.g.,copying,
   office supplies, postage,      
   freight, consulting,
   honoraria)

F. TRAVEL                  2,300.            2,300.           2,300.
   All Domestic Travel

G. PUBLICATIONS	           1,200.            1,200.           1,200.

H. OTHER COSTS             8,300.            8,300.           8,300.
   1.Communication  2,000.
     (telephone)     
   2. Computer      6,300.
      Equip. Maint.
                          _______          ________          _______  

I. TOTAL COSTS             82,145.          88,044.          94,510.
    (A through H)

J. INDIRECT COSTS:58% of   47,644.          51,066.          54,816.
   A through H, less D.   ________         ________         ________     


K. TOTAL COSTS            129,789.         139,110.         149,326.
.end "budget"
.twocol;↓ESDv4⊂λ$$V4n≤<≡'&Gα+λ	%H_;LD⊂∧0|YyP P,¬∀LJD@Pbrβ1e%α≤¬vn(⊂λ (iloc@=aQSGα1αC⊗{ &]↑2ε7-yPhWMR¬∨L≥f'ε⎇_ND≠yHλ≡]~0∪~qtpvλ$w:2[64sr[1rW %2Machi`≥J↓∪]iKαc3'∨.s∂*ε@	&∃β"\∞¬H
≠T¬502 (eds MelTzer, B. and @≠Sα≠#'∃bα⊃9%rα↔∪'v∪WK∨CQαπ∪Ns@/,⎇hU]m↔6/.8
.O(∀⊂→→yyWεB∧@
%3McCarthp∩X↓∀\Jbα↓!Ee9;¬%αnK;'\≥B∧Nlh	.,8π1`% - A↓≥KnA]CrA↑α1α+Woβ';≤hSS-α≤¬vv≡L↑6N}n4αG&t&*π∞XλMM<z→,E+C"AQI,s,8x<]
∂+λ∩EdαXP∀\[[q
P#4y≤z⊂'`2der The`∨e%KfA←_A∪MI%mSIk¬XAπ←9G@↔C'_4)#&yβ∃πβW3O≠#↔⊃Jp4(4R)N7∞≡KS#Jaα)9+	↓!EK9←
%∧O∂KN∪';≥∧k↔;S∞aαGW∞c'S'/→βS=∧kπ∂#Ns↔M↓G#<4+⊗)βCW⊗c'O#.!%84Ph)∃Nn{?K∃bαK?/∪Qα
r)E↓!I]]%¬∪↔πO}s';≥ε?W ∧∧↑v}⎇F.&|Tε∞vDλ⊗∨&≥⎇bbαV"∪K;qQ$LT8→∩¬π-x6..M≥f/~V∃`hPQ$S≤n8<↔↔&∂∃B∧Rd∧S
C↔⊗s>"∀λfO↔>ET␈⊗LZ"¬⊗↑λL↑y;]≡~;{D
yH∀L\⎇<\m≡Y(∀∞-y|X-↑kβ"E∞≠h_LT≤≥8MM<z→,E+C"AQUy>-∞X=8m¬λ⊃SiD≠8;N\;λm{λ≤∞-{yH={≠→,>~;{ED_<]
≤{→(
⎇H→[mA"KY-lβ"@↓E\zz.∧Lπ1"S[nL<h→M}H∪Thd≤≤[n
|x;↓QC"Um=∞H
∞[{qDz→8m=;Yk∧<~<nL9;{
|}+λ|;Y<L≥λ_X.≥8h∀L↑y8<L=C"AQUz_.D~_<dY9;D≠{Y'$⊃⊂qED⊃Ss¬D∪8pn4→<∩.>→;;mMy}(≥Yλ∪*HiC"AQUz≠g$∃y>-∞X=0m¬λ∩S(4≤_<ND≥~;,Uλ≤Y.<8<Xm∧→Y;
M⎇h_.∀≥Z<m≡≠|K∧ελ→|L≤≥8=Q"\⎇∞\→;]∞5λ→~.=h→Z-L+λ≥↑[:;L≥≤kC!!"T≥,-~8x.M;{\g!"C"A~Y8y-n≠≡(
My→λ
|9{Y.$_{{.
→=→,D_(≥
<z<d¬∃x9ml<H'⊗mj(
⎇C"Z≡Y≥x.,(≥Y.-9Z8l≡~;{D∞<z;Lt⊃Ss¬dλ∩=∧∞≥<[N4≠⎇=∧∞~_=∧;≠;n>λ_;
A"Z_.,≥x<LT≥Y<M≤Z8x.M;{H
<h≥.<9λ≤m≥=;_.M;{K∧;Yλ∞=;=;≡~;{Dx;C!-Y=Y.$_Y(={<≠↑→+H∧
x9{L↑H~_.4≤z≠n⎇H≥~≡λ≤≤M}Z;Yd
_<Y∞|<Y(=|\Y,>β"X.D≥~→$
→=Y-D≠yH|=→<d;Yλm~<,m≠|≤d
<h≥l]≠λ≤n]=→9∧∞≠h≤∞-{yK,=→8zm≥Ykβ!,Y8x.↑y(≥
(≤≤M|[→;.4≠yH
\=~→-\=~8l≥λ~;LN8⎇~-⎇H≥~≡λ_<M≡y(~-d≤≤[l}X;#!.Y<Z,m8x=
≥{H≥.>8;≠∂∀→≠{D}λ_<M≡y+C!!"B5
(_<∞
~8x.M;{H
|H→Z..⎇λ≠n,→<H
Myz8d∞≠h≥L↑Z9↑-≥Yh≤∞-y|X-↑c"Z≡h_Y,]H≤⎇
≥=;_.L9λ_O∀≥~→$~<xm}Y<↑$¬∪8pl≡]~≡$ε.-ml5(≥~≡λ≤Y,><\z.l#"\∞-y|X-↑h_x-d_Y(
m8y;∂∀_z_.,8⎇→.->Y9∧↑(_$Z<\nD≠|Y↑H→]-l⎇~;ml;β"L↑=8=
≥{H_-lλ_(m<\⎇∧
|Y→.$≠:;M≥:>X.M;{H∞<z→;,∃Hλ⊂-M;|u∧;≠λ∞,8<{ml8[→!QY>≥]\z;ml;λ≤∞-|→<NM9<h
|H≤≥.,(∪∩*:λ≤∀M||X;.4≤z≠n]→λ_LT_{{Nl;Z9-n≠≡(↓Q\≤[nl8[→%dλ∃y$∞≤[|
}y(≥
t~;]L↑⎇~9l≡→(≥
<y(∞≡9<p~~ww9P→8¬rther in the
next time period.